﻿using System;
using System.Diagnostics;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Text.RegularExpressions;
using System.Threading.Tasks;

using alib;
using alib.Enumerable;
using alib.Debugging;

namespace agree
{
	///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
	/// 
	///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
	public struct SkolemizationResult
	{
		public SkolemizationResult(Tfs tfs, CoverageMap w)
		{
			this.tfs = tfs;
			this.w = w;
		}
		[DebuggerBrowsable(DebuggerBrowsableState.RootHidden)]
		public readonly Tfs tfs;
		public CoverageMap w;
	};

	///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
	/// 
	///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
	public class RelMatchHelper : identity_base,
		schema.ρρMrsManager
	{
		public RelMatchHelper(MrsManager mrsm)
			: base(mrsm)
		{
			this.mrsm = mrsm;

		}

		//TfsUnifier fsu;
		//public TfsUnifier TfsUnifier
		//{
		//	get { return fsu; }
		//	set { fsu = value; }
		//}

		//FeatMgr ftm { get { return mrsm.ftm; } }


		readonly MrsManager mrsm;
		public MrsManager MrsManager
		{
			get { return mrsm; }
			set { throw not.valid; }
		}

		public struct RelIndex
		{
			public RelIndex(int index, TfsSlot rel)
			{
				this.index = index;
				this.rel = rel;
			}

			public int index;
			public TfsSlot rel;
		};

		public class RelMatch : List<int>, IIdentMasterGroup<int>
		{
			public RelMatch(int key, IEnumerable<int> rels)
				: base(rels)
			{
				this.key = key;
			}
			public readonly int key;
			public int Key { get { return key; } }
			Object IGrouping.Key { get { return key; } }
			public override string ToString()
			{
				return String.Format("{0} {1}", key, this.StringJoin(" "));
			}
			public IIdentity Trace { get { return null; } }
		};


		public struct ConsolidatedRelPairing
		{
			public ConsolidatedRelPairing(IEnumerable<Pairing<RelIndex>> rel_pairings)
			{
				this.rel_pairings = rel_pairings;
			}

			readonly IEnumerable<Pairing<RelIndex>> rel_pairings;

			public IEnumerable<Pairing<int>> IndexPairings
			{
				get { return rel_pairings.Select(pr => new Pairing<int>(pr.x.index, pr.y.index)); }
			}

			public IEnumerable<Pairing<ITfsSlot>> TfsSlotPairings
			{
				get { return rel_pairings.Select(pr => new Pairing<ITfsSlot>(pr.x.rel, pr.y.rel)); }
			}

			public ulong y_bitmask(out int c)
			{
				c = 0;
				ulong ul = 0;
				foreach (var pr in rel_pairings)
				{
					ul |= 1UL << pr.y.index;
					c++;
				}
				return ul;
			}
		};

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// 
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////

		public IEnumerable<SkolemizationResult> EnumerateSkolemizationResults(GenerationInput input, ITfsSlot candidate)
		{
			var candidate_rels = mrsm.GetRelSlots(candidate);
			var reference_rels = mrsm.GetRelSlots(input.ts_mrs);

			Debug.Assert(candidate_rels.Length <= reference_rels.Length);

			foreach (var rel_pairing in EnumerateRelPairings(candidate_rels, reference_rels))
			{
				var sktfs = Unification.UnifySectionsIntoShell(candidate.Tfs, rel_pairing.TfsSlotPairings, Tfs.Flags.WantVarbits);
				if (sktfs != null)
				{
					/// bit positions in the *candidate's* coverage bitmask are indexes of the *reference* rels
					int c;
					ulong ep_coverage = rel_pairing.y_bitmask(out c);

					yield return new SkolemizationResult(sktfs, new CoverageMap(input, ep_coverage, c, sktfs.varbits));
				}
			}
		}

		public IEnumerable<ConsolidatedRelPairing> EnumerateRelPairings(TfsSlot[] candidate_rels, TfsSlot[] reference_rels)
		{
			Debug.Assert(candidate_rels.Length <= reference_rels.Length);

			foreach (var match_set in candidate_rels
										.Select((cr, ix) => new RelMatch(ix, reference_rels.IndiciesWhere(rr => mrsm.ComparePred(cr, rr))))
										.GroupCrossProduct())
			{
				var q = match_set.Select(pr => new Pairing<RelIndex>(
					new RelIndex(pr.x, candidate_rels[pr.x]),
					new RelIndex(pr.y, reference_rels[pr.y])));

				yield return new ConsolidatedRelPairing(q);
			}
		}

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// OLD VERSION
		/// used by TriggerRule -> CheckRule -> IsSatisfiedBy
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		public bool CompareRels(TfsSlot[] rels1, TfsSlot[] rels2, bool f_pred_restrict = false, bool f_subsumption = false)
		{
			return EnumerateRelPairings(rels1, rels2).Any(rel_pairings =>
			{
				if (f_subsumption)
				{
					/// This hasn't been fully verified as working. The idea is to enable it for certain trigger rules.
					int sdir = Subsumption.CheckSubsumptionPairs(mrsm.ftm.GenerationRestrictors.r_pack, rel_pairings.TfsSlotPairings);
					return sdir == Subsumption.FirstSubsumesSecond;
				}
				else
				{
#if false
					throw new Exception("gcs: 4/7/2013 pred restrict not implemented in unifier any more. see 510-unify-control.cs");
					if (f_pred_restrict)
						;// opts |= Tfs.Flags.PredRestrict;
					var r = ftm.GenerationRestrictors.FromTfsFlags(opts);
#endif
					return Unification.CheckMultipleNodePointers(mrsm.PredRestrict, rel_pairings.TfsSlotPairings);
				}
			});
		}



		//public bool HasExtraneousContentFor(TfsSlot ts_mrs_le, TfsSlot ts_input_mrs)
		//{
		//	var le_slots = mrsm.GetRelSlots(ts_mrs_le);
		//	if (le_slots == null)
		//		return false;

		//	var input_slots = mrsm.GetRelSlots(ts_input_mrs);

		//	return !(le_slots.All(le => input_slots.Any(inp => mrsm.ComparePred(inp, le))));
		//}

#if false
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// NEW VERSION
		/// used by gxo/unpack/Validate, and above
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		public bool CompareRels(ITfsSlot ts_mrs1, ITfsSlot ts_mrs2, bool f_pred_restrict = false, bool f_subsumption = false)
		{
			return EnumerateRelPairings(ts_mrs1, ts_mrs2).Any(pairs =>
			{
				if (f_subsumption)
				{
					/// This hasn't been fully verified as working. The idea is to enable it for certain trigger rules.
					int sdir = Subsumption.CheckSubsumptionPairs(TfsUnifier, pairs.Select(p => new Pairing<ITfsSlot>(p.x.rel, p.y.rel)));
					return sdir == Subsumption.FirstSubsumesSecond;
				}
				else
				{
					return Unification.CheckMultipleNodePointers(TfsUnifier, f_pred_restrict, pairs.Select(p => new Pairing<ITfsSlot>(p.x.rel, p.y.rel)));
				}
			});
		}
		public IEnumerable<IEnumerable<Pairing<RelIndex>>> EnumerateRelPairings(ITfsSlot candidate, ITfsSlot reference)
		{
			TfsSlot[] candidate_rels = mrsm.GetRelSlots(candidate);
			TfsSlot[] reference_rels = mrsm.GetRelSlots(reference);

			return EnumerateRelPairings(candidate_rels, reference_rels);
		}
#endif

		//public sealed class RegexPredComparerTs : IEqualityComparer<ITfsSlot>
		//{
		//	public RegexPredComparerTs(MrsManager mrsm)
		//	{
		//		this.mrsm = mrsm;
		//	}

		//	MrsManager mrsm;

		//	public bool Equals(ITfsSlot x, ITfsSlot y)
		//	{
		//		var x_flag = new TfsSlot(x)[mrsm.ifeat_pred].EdgeFlag;
		//		var y_flag = new TfsSlot(x)[mrsm.ifeat_pred].EdgeFlag;

		//		if (x.Tfs.trigger_rule_regexes.ContainsKey(x.SlotIndex))
		//		{
		//			Console.Write("x");
		//			return x.Tfs.trigger_rule_regexes[x.SlotIndex].IsMatch(mrsm.tu.TypeNameOrStringValue(y_flag));
		//		}

		//		if (y.Tfs.trigger_rule_regexes.ContainsKey(y.SlotIndex))
		//		{
		//			Console.Write("y");
		//			return y.Tfs.trigger_rule_regexes[y.SlotIndex].IsMatch(mrsm.tu.TypeNameOrStringValue(x_flag));
		//		}
		//		//Console.Write("?");

		//		if (x_flag == 0 || y_flag == 0 || x_flag == y_flag)
		//			return true;
		//		if ((x_flag & y_flag) >= Edge.Flag.EtmLeafType)
		//			return false;
		//		return (x_flag < y_flag ? mrsm.tu.UnifyTypesHiLo(x_flag, y_flag) : mrsm.tu.UnifyTypesHiLo(y_flag, x_flag)) >= 0;
		//	}

		//	public int GetHashCode(ITfsSlot rel)
		//	{
		//		Console.Write("0");
		//		return 0;
		//		//return rel.regex != null ? 0 : rel.GetHashCode();
		//	}
		//};
	}
}
